package pl.edu.pw.elka.dzielins.revanalyzer.alloy.io;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Collections;
import java.util.Comparator;
import java.util.LinkedList;
import java.util.List;
import java.util.StringTokenizer;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import javax.xml.parsers.FactoryConfigurationError;

import org.apache.commons.lang3.StringUtils;
import org.apache.log4j.Logger;

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.Pair;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4compiler.ast.Attr;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Decl;
import edu.mit.csail.sdg.alloy4compiler.ast.Expr;
import edu.mit.csail.sdg.alloy4compiler.ast.ExprHasName;
import edu.mit.csail.sdg.alloy4compiler.ast.ExprUnary;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.SubsetSig;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import pl.edu.pw.elka.dzielins.revanalyzer.Project;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.AlloyException;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.AlloyLogger;
import pl.edu.pw.elka.dzielins.revanalyzer.model.Arity;
import pl.edu.pw.elka.dzielins.revanalyzer.model.Model;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelFact;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelObject;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelRelation;

//TODO univ none itp.
public class Reader {
	private static final Logger LOG = Logger.getLogger(Reader.class);
	private static final Pattern NAME_PATTERN = Pattern.compile("(?:this|[a-zA-Z]+)(?:/[a-zA-Z]+)*");
	private static final Pattern FIELD_DECLARATION_PATTERN = Pattern.compile("(some|one|lone|set)?\\s*((?:[a-zA-Z0-9/]+|[a-zA-Z/]*\\s*\\.?\\s*\\([a-zA-Z0-9/]+ <: [a-zA-Z0-9/]+\\))(?:\\s*->\\s*[a-zA-Z0-9/]+|[a-zA-Z0-9/]*\\s*\\.?\\s*\\([a-zA-Z0-9/]+ <: [a-zA-Z0-9/]+\\))*)");
	private static final Pattern RELATION_PATTERN = Pattern.compile("[a-zA-Z/]*\\s*\\.?\\s*\\([a-zA-Z/]+ <: ([a-zA-Z/]+)\\)");
	private static final Pattern COMPLEX_FACT_PATTERN = Pattern.compile("AND\\[(.*)\\]");
	
	private Project currentProject;
	private Module modelModule;
	
	public Project readAlloy(String instancePath, String modelPath) throws Exception
	{
		if (StringUtils.isBlank(modelPath))
			throw new AlloyException("invalid Model file");
		File modelFile = new File(modelPath);
		if (!modelFile.exists())
			throw new AlloyException("invalid Model file");
		currentProject = new Project();
		Model model, instance;
		// read modules
		A4Reporter reporter = new AlloyLogger();
		// read model module(s)
		modelModule = null;
		LOG.debug("Reading Model from " + modelFile.getPath());
		try {
			modelModule = CompUtil.parseEverything_fromFile(reporter, null, modelFile.getPath());
		} catch (Err e) {
			// TODO exception handling
			e.printStackTrace();
			/*if (e.getCause() instanceof FileNotFoundException)
				throw new AlloyException("File " + modelPath +" not found!", e.getCause());*/
		}
		currentProject.getModel().setModule(modelModule);
		currentProject.getModel().setModulePath(modelFile.getPath());
		readModel();
		
		// get facts and commands
		List<Pos> toStrip = new LinkedList<Pos>();
		for (Pair<String,Expr> fact : modelModule.getAllFacts()) {
			toStrip.add(fact.b.pos);
		}
		for (Command comm : modelModule.getAllCommands()) {
			toStrip.add(comm.pos);
		}
		// sort list by position
		Collections.sort(toStrip, new Comparator<Pos>() {
			@Override
			public int compare(Pos o1, Pos o2) {
				if (o1.y==o2.y) {
					return Integer.compare(o1.x, o2.x);
				} else {
					return Integer.compare(o1.y, o2.y);
				}
			}
		});
		// created stripped model file
		int lineNumber = 1;
		int i = 0;
		String line;
		boolean read = true;
		File strippedModel = new File("strippedModel");
		if (!strippedModel.exists())
			strippedModel.createNewFile();
		BufferedWriter writer = new BufferedWriter(new FileWriter(strippedModel));
		writer.flush();
		BufferedReader reader = new BufferedReader(new FileReader(modelPath));
		if (toStrip != null && !toStrip.isEmpty()) {
			while ((line = reader.readLine()) != null) {
				if (lineNumber<toStrip.get(i).y) {
					writer.write(line);
					writer.newLine();
				} else if (lineNumber==toStrip.get(i).y) {
					writer.write(StringUtils.substring(line, 0, toStrip.get(i).x-1));
					writer.newLine();
				} else if (lineNumber==toStrip.get(i).y2) {
					writer.write(StringUtils.substring(line, toStrip.get(i).x2));
					writer.newLine();
					i++;
				}
				lineNumber++;
			}
		}
		reader.close();
		writer.close();
		// save declarations to facts
		List<ModelFact> facts = new LinkedList<ModelFact>(currentProject.getModel().getFacts());
		Collections.sort(facts, new Comparator<ModelFact>() {
			@Override
			public int compare(ModelFact o1, ModelFact o2) {
				if (o1.getExpression().pos.y==o2.getExpression().pos.y) {
					return Integer.compare(o1.getExpression().pos.x, o2.getExpression().pos.x);
				} else {
					return Integer.compare(o1.getExpression().pos.y, o2.getExpression().pos.y);
				}
			}
		});
		if (!facts.isEmpty()) {
			i = 0;
			int l = 0;
			String[] declar;
			lineNumber = 1;
			declar = new String[facts.get(i).getExpression().pos.y2-facts.get(i).getExpression().pos.y+1];
			reader = new BufferedReader(new FileReader(modelPath));
			while ((line = reader.readLine()) != null) {
				if (lineNumber==facts.get(i).getExpression().pos.y) {
					declar[l] = StringUtils.substring(line, facts.get(i).getExpression().pos.x-1, line.length());
					l++;
				} else if (lineNumber>facts.get(i).getExpression().pos.y && lineNumber<facts.get(i).getExpression().pos.y2) {
					declar[l] = line;
					l++;
				} else if (lineNumber==facts.get(i).getExpression().pos.y2) {
					declar[l] = StringUtils.substring(line, 0, facts.get(i).getExpression().pos.x2);
					facts.get(i).setDeclaration(declar);
					l = 0;
					i++;
					if (i<facts.size()) {
						declar = new String[facts.get(i).getExpression().pos.y2-facts.get(i).getExpression().pos.y+1];
					} else {
						break;
					}
				}
				lineNumber++;
			}
			reader.close();
		}
		
		return currentProject;
	}
	
	private void readModel() {
		if (modelModule==null)
			return;	
		// read signatures
		for (Sig sig : modelModule.getAllReachableSigs()) {
			readModelSig(sig);
		}
		// read facts
		for (Pair<String, Expr> fact : modelModule.getAllFacts()) {
			readModelFact(fact);
		}
	}
	
	/**
	 * ModelObject is added to the current project model.
	 * @param sig 
	 * @return ModelObject based on given Sig.
	 */
	private ModelObject readModelSig(Sig sig) {
		// TODO remove univ
		// omit built-in signatures (univ, Int etc.)
		if (sig==null||sig.builtin)
			return null;
		ModelObject object = null;
		// check if signature was read before
		object = currentProject.getModel().getObject(convertSigLabel(sig.label));
		if (object != null)
			return object;		
		boolean isSubsig = sig.isSubsig != null;
		boolean isSubset = sig.isSubset != null;
		try {
			if (isSubsig && !isSubset)
				object = readModelPrimSig((PrimSig) sig);
			else if (!isSubsig && isSubset)
				object = readModelSubSig((SubsetSig) sig);
			else {
				// TODO handling isSubsig&&isSubset and !isSubsig&&!isSubset
			}
		} catch (ClassCastException e) {
			// TODO exception handling
			e.printStackTrace();
		}
		return object;
	}

	private ModelObject readModelSubSig(SubsetSig sig) {
		// TODO Auto-generated method stub
		return null;
	}

	private ModelObject readModelPrimSig(PrimSig sig) {
		ModelObject object = new ModelObject();
		// set name
		object.setName(convertSigLabel(sig.label));
		// add to model
		currentProject.getModel().getObjects().add(object);
		LOG.debug("Reading signature: " + object.getName());
		// set signature
		object.setSig(sig);
		// set base object
		if (sig.isTopLevel()) {
			object.setBaseObject(null);
		} else {
			ModelObject baseObject = currentProject.getModel().getObject(
					convertSigLabel(sig.parent.label));
			if (baseObject == null)
				baseObject = readModelSig(sig.parent);
			if (baseObject == null && !sig.parent.builtin)
				// TODO exception handling
				throw new RuntimeException("base object not found");
			object.setBaseObject(baseObject);
		}
		// read relations
		// TODO difference between Decl and Field (disjoint)
		for (Field relationField : sig.getFields()) {
			// System.out.println("F"+field.toString()+";"+field.decl().names.toString()+";"+field.decl().expr);
			ModelRelation relation = readModelRelation(relationField,object);
			// System.out.println(relation.toString());
			if (relation != null)
				object.getRelations().add(relation);
		}
		return object;
	}
	
	private ModelRelation readModelRelation(Field relationField, ModelObject owner) {
		if (relationField == null)
			return null;
		Decl relationDecl = relationField.decl();
		// TODO why list of names is returned?!
		String name = convertFieldName(relationDecl.names.get(0).toString());
		Expr expression = relationDecl.expr;
		
		// Relation can contain other relations
		Matcher relationMatcher = FIELD_DECLARATION_PATTERN.matcher(expression.toString());
		if (!relationMatcher.matches())
			return null;
		LOG.debug("Reading field "+name+" declared as "+expression.toString());
		List<ModelObject> elements = new LinkedList<ModelObject>();
		for(String s:StringUtils.splitByWholeSeparator(relationMatcher.group(2), " -> ")) {
			// check if expression is relation
			Matcher elementMatcher = RELATION_PATTERN.matcher(s);
			if (elementMatcher.matches()) {
				//System.out.println(elementMatcher.group(1));
				//elements.add((ModelRelational) owner.getRelation(elementMatcher.group(1)));
				ModelRelation innerRelation = owner.getRelation(elementMatcher.group(1));
				elements.addAll(innerRelation.getArguments());
			}
			else {
				ModelObject elementObject = currentProject.getModel().getObject(convertSigLabel(s));
				if (elementObject==null)
					elementObject=readModelSig(findModuleSig(convertSigLabel(s)));
				if (elementObject==null)
					//TODO exception handling
					throw new RuntimeException("element object not found");
				elements.add(elementObject);
			}
		}
		ModelRelation relation = new ModelRelation(owner, name,relationField,elements.toArray(new ModelObject[]{}));
		return relation;
	}
	
	private void readModelFact(Pair<String,Expr> factDeclaration) {
		if (StringUtils.isBlank(factDeclaration.b.toString()))
			return;
		LOG.debug("Reading fact: " + factDeclaration.a);
		// there may me multiple facts in single fact declaration
		Matcher factMatcher = COMPLEX_FACT_PATTERN.matcher(factDeclaration.b.toString());
		ModelFact fact;
		/*try {
			if (factMatcher.matches()) {
				// complex fact
				String[] declarations = StringUtils.split(factMatcher.group(1), ",");
				for (int i = 0; i < declarations.length; ++i) {
					Expr expr = CompUtil.parseOneExpression_fromString(modelModule, declarations[i].trim());
					//ModelFact fact = new ModelFact(factDeclaration.a+" "+i, StringUtils.remove(declarations[i].trim(), "this/"));
					fact = new ModelFact(factDeclaration.a+" "+i, expr);
					currentProject.getModel().getFacts().add(fact);
				}
			} else {*/
				//ModelFact fact = new ModelFact(factDeclaration.a, StringUtils.remove(factDeclaration.b.toString().trim(), "this/"));
				fact = new ModelFact(factDeclaration.a, factDeclaration.b);
				currentProject.getModel().getFacts().add(fact);
			//}
		/*} catch (Err e) {
			e.printStackTrace();
		}*/
	}
	
	private Sig findModuleSig(String name) {
		if (modelModule==null || StringUtils.isBlank(name))
			return null;
		for(Sig sig : modelModule.getAllReachableSigs()) {
			if (name.equals(convertSigLabel(sig.label)))
				return sig; }
		return null;
	}
	
	private String convertFieldName(String name) {
		return StringUtils.substringBetween(name, " <: ", ")");
	}
	
	private String convertSigLabel(String label) {
		// From Alloy 4 grammar:
		// name ::= ["this" | ID] ["/" ID]*
		String s = StringUtils.substringAfter(label, "this/");
		//String s = StringUtils.substringAfter(label, "/");
		if (StringUtils.isBlank(s)) {
			s = label;
		}
		//return s.replace("/", ".");
		return s;
	}
}
